Manually merged to master. The automation is still failing, but I don't currently have time to investigate further.

@lemmy I would have been happy to help the user through the failures??? This PR happened when I was asleep.

@ahelwer Could the CI (Python scripts) automatically generate or infer most of the contents of manifest.json? If the scripts can verify consistency across the Spec/Model, Readme.md, and manifest.js, it seems plausible that manifest.json could be largely autogenerated (the state-space information could be a comment in the cfg file).

I agree the process is too complicated and am writing up an issue for some proposed improvements.

I opened an issue on simplifying the process in #171. To answer your question:

Could the CI (Python scripts) automatically generate or infer most of the contents of manifest.json?

There are some aspects of manifest.json that can be inferred & thus generated:

• The set of models & specs in the repository, from a simple file search
• The relation of models to specs, assuming they follow the recommended naming conventions
• Various properties like whether the specs contain proofs, whether the modules use symmetry, etc.

However, there are others which cannot be inferred:

• Expected model runtime
• Desired model execution mode (symbolic, exhaustive, simulate, generate)
• Expected model result (safety failure, liveness failure, deadlock, etc.)
• Expected state counts (as you observed)
• All the "soft" fields (name, description, authors, tags like "beginner", etc.)

• Expected model runtime
• Desired model execution mode (symbolic, exhaustive, simulate, generate)
• Expected model result (safety failure, liveness failure, deadlock, etc.)
• Expected state counts (as you observed)
• All the "soft" fields (name, description, authors, tags like "beginner", etc.)

All of this information can be included in either the preamble or postamble of the .tla specification, as well as within comments in the .cfg file. Thus, a manually maintained, centralized manifest.json file is unnecessary.